theory Design_OpenSession
imports "../DesignSpec"
begin
section "auxiliary function"
definition TA_OpenSessionEntryPointR::"Sys_Config⇒StateR⇒TEEC_Operation⇒THREAD_ID_TYPE⇒StateR" where
"TA_OpenSessionEntryPointR sc s opt tid≡
let s'=s⇓(TA_OpenSessionEntryPoint sc (⇑s) opt tid) in
s'⦇IPC_driver:=IPC_driver s⦈
"
definition ioctrlR :: "Sys_Config⇒StateR⇒TA_UUID_TYPE⇒TEEC_Operation⇒CLIENT_TYPE⇒TEEC_CONTEXT_TYPE
⇒(MemBlock × TEEC_MEMREF_TYPE )⇒(StateR×TEEC_RET_ORIGIN×TEEC_RESULT×SESSION_ID_TYPE)" where
"ioctrlR sc s uuid opt cli ctx1 mem_t0≡
let s'= (ioctrl sc (⇑s) uuid opt cli ctx1 mem_t0) in (s⇓(fst s'),fst(snd s'),fst(snd(snd s')),snd(snd(snd s')))"
section "Context"
definition TEEC_InitializeContextR ::"Sys_Config⇒StateR⇒TEE_NAME⇒TEEC_CONTEXT_TYPE option⇒(StateR × TEEC_CONTEXT_TYPE × TEEC_RESULT)" where
"TEEC_InitializeContextR sc s name ctx1 ≡ let s'= (TEEC_InitializeContext sc (⇑s) name ctx1) in (s⇓(fst s'),fst(snd s'),snd(snd s'))"
definition TEEC_FinalizeContextR :: "Sys_Config⇒StateR⇒TEEC_CONTEXT_TYPE option⇒StateR" where
"TEEC_FinalizeContextR sc s ctx1 ≡ let s'=(TEEC_FinalizeContext sc (⇑s) ctx1) in (s⇓s')"
section "TEEC_OpenSession"
definition TEEC_OpenSession1R :: "Sys_Config⇒StateR⇒TEEC_CONTEXT_TYPE option⇒TEEC_SESSION_TYPE option
⇒TA_UUID_TYPE⇒Connection_Method⇒Connection_Data
⇒TEEC_Operation option⇒(MemBlock × TEEC_MEMREF_TYPE )
⇒(StateR × TEEC_RET_ORIGIN × TEEC_RESULT)" where
"TEEC_OpenSession1R sc s ctx1 ses1 id1 md str opt mem_t≡
let s'= (TEEC_OpenSession1 sc (⇑s) ctx1 ses1 id1 md str opt mem_t) in (s⇓(fst s'),fst(snd s'),snd(snd s'))"
definition TEEC_OpenSession2R :: "Sys_Config⇒StateR⇒(StateR × TEEC_RET_ORIGIN × TEEC_RESULT ×SESSION_ID_TYPE)" where
"TEEC_OpenSession2R sc s ≡
if current s ≠ TEE sc
then (s,TEEC_ORIGIN_TEE,TEEC_ERROR_BUSY,INVALID_SESSION_ID)
else
if (exec_prime s) =[]
then (s,TEEC_ORIGIN_TEE,TEEC_ERROR_BUSY,INVALID_SESSION_ID)
else
if snd (hd (exec_prime s)) ≠TEEC_OP2
then (s,TEEC_ORIGIN_TEE,TEEC_ERROR_BUSY,INVALID_SESSION_ID)
else
let exec = (exec_prime s);
s1= s⦇exec_prime:=tl exec⦈;
p = fst (hd (exec));
uuid = the (param1 p);
opt = param3 p;
cli = the (param4 p);
ctx1 = param5 p ;
mem_t = (the (param10 p),the (param11 p));
s2 = Driver_Read s1 smc_ex_init_read zx_mgr
in
ioctrlR sc s2 uuid (the opt) cli (the ctx1) mem_t"
definition TEEC_OpenSession3R :: "Sys_Config⇒StateR⇒SESSION_ID_TYPE⇒(StateR × TEEC_RET_ORIGIN × TEEC_RESULT ×SESSION_ID_TYPE)" where
"TEEC_OpenSession3R sc s sid≡
if (exec_prime s) =[]
then (s,TEEC_ORIGIN_TEE,TEEC_ERROR_BUSY,INVALID_SESSION_ID)
else
if snd (hd (exec_prime s)) ≠TEEC_OP3
then (s,TEEC_ORIGIN_TEE,TEEC_ERROR_BUSY,INVALID_SESSION_ID)
else
let exec = (exec_prime s);
s1= s⦇exec_prime:=tl exec⦈;
p = fst (hd (exec));
tid1 = the (param1 p);
ses_id = the (param2 p);
opt = param3 p;
ctx1 = the(param5 p) in
if sid≠ses_id ∨ current s=TEE sc ∨current s=REE sc∨tid1≠current s then (s,TEEC_ORIGIN_TEE,TEEC_ERROR_BUSY,INVALID_SESSION_ID)
else let
s2 = s1⇓(initTAProcess (⇑s1) (the opt) tid1 ses_id);
s3 = TA_OpenSessionEntryPointR sc s2 (the opt) tid1;
param=⦇param1=Some tid1,param2=Some ses_id,param3=None,param4=None,
param5=None,param6=None,param7=None,param8=None,param9=None,
param10=None,param11=None,param12=Some TEEC_SUCCESS,param13=None⦈;
s6= s3⦇current:=TEE sc,exec_prime:=(param,TEEC_OP4)#(exec_prime s3)⦈ in
(s6,TEEC_ORIGIN_TRUSTED_APP,TEEC_SUCCESS,ses_id)"
definition TEEC_OpenSession4R :: "Sys_Config⇒StateR⇒(StateR × TEEC_RET_ORIGIN × TEEC_RESULT ×SESSION_ID_TYPE)" where
"TEEC_OpenSession4R sc s ≡
if (exec_prime s) =[]
then (s,TEEC_ORIGIN_TEE,TEEC_ERROR_BUSY,INVALID_SESSION_ID)
else
if snd (hd (exec_prime s)) ≠TEEC_OP4
then (s,TEEC_ORIGIN_TEE,TEEC_ERROR_BUSY,INVALID_SESSION_ID)
else
let exec = (exec_prime s);
s1= s⦇exec_prime:=tl exec⦈;
p = fst (hd (exec));
tid1 = the (param1 p);
ses_id = the (param2 p);
res3= the (param12 p);
smc_ex = ⦇a0=0,a1=0,a2=0,a3= ses_id,a4=0,a5=0,a6=0,a7=0,u2k=0,k2u=0⦈;
sa=s1⇓(MgrPostOperation (⇑s1) tid1);
sar = fst(Driver_Write_smc sa zx_mgr ZX_OKr smc_ex);
param=⦇param1=Some ses_id,param2=Some tid1,param3=None,param4=Some ⦇login=DTC_IDENTITY,id=Some 0⦈,
param5=None,param6=None,param7=None,param8=None,param9=None,param10=None,param11=None,param12=None,param13=None⦈;
s2=sa⦇current:=TEE sc,exec_prime:=(param,TEEC_CS2)#(exec_prime sa)⦈;
s2r = fst(Driver_Write_smc s2 zx_mgr ZX_ERR_INTERNALr smc_ex_init)
in
if current s≠TEE sc then (s,TEEC_ORIGIN_TRUSTED_APP,TEEC_ERROR_BUSY,INVALID_SESSION_ID)
else if res3≠TEEC_SUCCESS then (s2r,TEEC_ORIGIN_TRUSTED_APP,TEEC_ERROR_BUSY,INVALID_SESSION_ID)
else
(sar,TEEC_ORIGIN_TRUSTED_APP,TEEC_SUCCESS,ses_id)"
section "TEE_OpenTASession"
definition TEE_OpenTASession1R :: "Sys_Config⇒StateR
⇒(StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE)" where
"TEE_OpenTASession1R sc s ≡
let s'= (TEE_OpenTASession1 sc (⇑s))
in (s⇓(fst s'),fst(snd s'),snd(snd s'))"
definition TEE_OpenTASession2R :: "Sys_Config⇒StateR
⇒(StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE × SESSION_ID_TYPE)" where
"TEE_OpenTASession2R sc s ≡
let s'= (TEE_OpenTASession2 sc (⇑s))
in (s⇓(fst s'),fst(snd s'),fst(snd(snd s')),snd(snd(snd s')))"
definition TEE_OpenTASession3R :: "Sys_Config ⇒ StateR ⇒SESSION_ID_TYPE
⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE × SESSION_ID_TYPE" where
"TEE_OpenTASession3R sc s sid ≡
let
exec = (exec_prime s);
s1= s⦇exec_prime:=tl exec⦈;
p = fst (hd (exec));
tid1 = the (param1 p);
ses_id = the (param2 p);
opt = param3 p;
ctx1 = the(param5 p);
s2 = s1⇓(initTAProcess (⇑s1) (the opt) tid1 ses_id);
s3 = TA_OpenSessionEntryPointR sc s2 (the opt) tid1;
param=⦇param1=Some tid1,param2=Some ses_id,param3=None,param4=None,
param5=None,param6=None,param7=None,param8=None,param9=None,param10=None,param11=None,param12=None, param13=Some TEE_SUCCESS⦈;
s5= s3⦇current:=TEE sc,exec_prime:=(param,TEE_OP4)#(exec_prime s3)⦈ in
if (exec_prime s) = [] ∨ snd (hd (exec_prime s)) ≠ TEE_OP3 ∨ sid ≠ ses_id∨ current s=TEE sc ∨current s=REE sc ∨ current s ≠ tid1 then
(s, TEE_ORIGIN_TEE, TEE_ERROR_BUSY, INVALID_SESSION_ID)
else
(s5, TEE_ORIGIN_TRUSTED_APP, TEE_SUCCESS,ses_id)"
definition TEE_OpenTASession4R :: "Sys_Config⇒StateR
⇒(StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE × SESSION_ID_TYPE)" where
"TEE_OpenTASession4R sc s ≡
let s'= (TEE_OpenTASession4 sc (⇑s))
in (s⇓(fst s'),fst(snd s'),fst(snd(snd s')),snd(snd(snd s')))"
end